Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(b(b(x1)))) → b(b(b(a(a(a(x1))))))
a(c(x1)) → c(a(x1))
b(c(x1)) → c(b(x1))
Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(b(b(x1)))) → b(b(b(a(a(a(x1))))))
a(c(x1)) → c(a(x1))
b(c(x1)) → c(b(x1))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(a(b(b(x1)))) → b(b(b(a(a(a(x1))))))
a(c(x1)) → c(a(x1))
b(c(x1)) → c(b(x1))
The set Q is empty.
We have obtained the following QTRS:
b(b(a(a(x)))) → a(a(a(b(b(b(x))))))
c(a(x)) → a(c(x))
c(b(x)) → b(c(x))
The set Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
b(b(a(a(x)))) → a(a(a(b(b(b(x))))))
c(a(x)) → a(c(x))
c(b(x)) → b(c(x))
Q is empty.
Termination of the TRS R could be shown with a Match Bound [6,7] of 7. This implies Q-termination of R.
The following rules were used to construct the certificate:
b(b(a(a(x)))) → a(a(a(b(b(b(x))))))
c(a(x)) → a(c(x))
c(b(x)) → b(c(x))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
121, 122, 123, 128, 127, 126, 125, 124, 129, 134, 133, 132, 131, 130, 139, 138, 137, 136, 135, 144, 143, 142, 141, 140, 149, 148, 147, 146, 145, 154, 153, 152, 151, 150, 159, 158, 157, 156, 155, 164, 163, 162, 161, 160, 169, 168, 167, 166, 165, 171, 172, 170, 174, 173, 179, 178, 177, 176, 175, 181, 182, 180, 184, 183, 186, 187, 185, 189, 188, 191, 192, 190, 194, 193, 196, 197, 195, 199, 198, 201, 202, 200, 204, 203, 206, 207, 205, 209, 208, 211, 212, 210, 214, 213, 227, 228, 226, 230, 229, 235, 236, 234, 238, 237
Node 121 is start node and node 122 is final node.
Those nodes are connect through the following edges:
- 121 to 123 labelled b_1(0), a_1(0), a_1(1)
- 121 to 124 labelled a_1(0)
- 122 to 122 labelled #_1(0)
- 123 to 122 labelled c_1(0)
- 123 to 129 labelled b_1(1), a_1(1)
- 123 to 140 labelled a_1(2)
- 128 to 122 labelled b_1(0)
- 128 to 130 labelled a_1(1)
- 127 to 128 labelled b_1(0)
- 127 to 130 labelled a_1(1)
- 126 to 127 labelled b_1(0)
- 126 to 135 labelled a_1(1)
- 125 to 126 labelled a_1(0)
- 124 to 125 labelled a_1(0)
- 129 to 122 labelled c_1(1)
- 129 to 129 labelled b_1(1), a_1(1)
- 129 to 140 labelled a_1(2), b_1(1)
- 129 to 141 labelled b_1(1)
- 134 to 122 labelled b_1(1)
- 134 to 130 labelled a_1(1)
- 133 to 134 labelled b_1(1)
- 133 to 130 labelled a_1(1)
- 132 to 133 labelled b_1(1)
- 132 to 145 labelled a_1(2)
- 131 to 132 labelled a_1(1)
- 130 to 131 labelled a_1(1)
- 139 to 131 labelled b_1(1)
- 138 to 139 labelled b_1(1)
- 138 to 155 labelled a_1(2)
- 137 to 138 labelled b_1(1)
- 136 to 137 labelled a_1(1)
- 135 to 136 labelled a_1(1)
- 144 to 129 labelled b_1(2)
- 144 to 140 labelled a_1(2), b_1(2)
- 144 to 141 labelled b_1(2)
- 144 to 142 labelled b_1(2)
- 144 to 150 labelled a_1(3), b_1(2)
- 143 to 144 labelled b_1(2)
- 143 to 140 labelled a_1(2)
- 143 to 150 labelled a_1(3)
- 143 to 175 labelled a_1(3)
- 142 to 143 labelled b_1(2)
- 142 to 150 labelled a_1(3)
- 141 to 142 labelled a_1(2)
- 140 to 141 labelled a_1(2)
- 149 to 131 labelled b_1(2)
- 148 to 149 labelled b_1(2)
- 148 to 155 labelled a_1(2)
- 147 to 148 labelled b_1(2)
- 146 to 147 labelled a_1(2)
- 145 to 146 labelled a_1(2)
- 154 to 141 labelled b_1(3)
- 154 to 142 labelled b_1(3)
- 154 to 150 labelled a_1(3)
- 154 to 151 labelled b_1(3)
- 154 to 152 labelled b_1(3)
- 154 to 176 labelled b_1(3)
- 154 to 190 labelled a_1(4)
- 153 to 154 labelled b_1(3)
- 153 to 170 labelled a_1(4)
- 153 to 175 labelled a_1(3)
- 153 to 190 labelled a_1(4)
- 152 to 153 labelled b_1(3)
- 152 to 170 labelled a_1(4)
- 152 to 190 labelled a_1(4)
- 151 to 152 labelled a_1(3)
- 150 to 151 labelled a_1(3)
- 159 to 145 labelled b_1(2)
- 158 to 159 labelled b_1(2)
- 158 to 160 labelled a_1(3)
- 157 to 158 labelled b_1(2)
- 156 to 157 labelled a_1(2)
- 155 to 156 labelled a_1(2)
- 164 to 147 labelled b_1(3)
- 164 to 165 labelled a_1(3)
- 163 to 164 labelled b_1(3)
- 162 to 163 labelled b_1(3)
- 162 to 180 labelled a_1(4)
- 161 to 162 labelled a_1(3)
- 160 to 161 labelled a_1(3)
- 169 to 156 labelled b_1(3)
- 168 to 169 labelled b_1(3)
- 167 to 168 labelled b_1(3)
- 166 to 167 labelled a_1(3)
- 165 to 166 labelled a_1(3)
- 171 to 172 labelled a_1(4)
- 172 to 173 labelled b_1(4)
- 170 to 171 labelled a_1(4)
- 174 to 151 labelled b_1(4)
- 174 to 170 labelled b_1(4)
- 174 to 190 labelled b_1(4)
- 173 to 174 labelled b_1(4)
- 173 to 170 labelled a_1(4)
- 173 to 205 labelled a_1(5)
- 179 to 150 labelled b_1(3)
- 178 to 179 labelled b_1(3)
- 178 to 185 labelled a_1(4)
- 177 to 178 labelled b_1(3)
- 176 to 177 labelled a_1(3)
- 175 to 176 labelled a_1(3)
- 181 to 182 labelled a_1(4)
- 182 to 183 labelled b_1(4)
- 180 to 181 labelled a_1(4)
- 184 to 166 labelled b_1(4)
- 183 to 184 labelled b_1(4)
- 186 to 187 labelled a_1(4)
- 187 to 188 labelled b_1(4)
- 187 to 200 labelled a_1(5)
- 185 to 186 labelled a_1(4)
- 189 to 152 labelled b_1(4)
- 189 to 190 labelled a_1(4)
- 188 to 189 labelled b_1(4)
- 188 to 195 labelled a_1(5)
- 188 to 200 labelled a_1(5)
- 191 to 192 labelled a_1(4)
- 192 to 193 labelled b_1(4)
- 190 to 191 labelled a_1(4)
- 194 to 171 labelled b_1(4)
- 194 to 176 labelled b_1(4)
- 194 to 191 labelled b_1(4)
- 193 to 194 labelled b_1(4)
- 196 to 197 labelled a_1(5)
- 197 to 198 labelled b_1(5)
- 195 to 196 labelled a_1(5)
- 199 to 171 labelled b_1(5)
- 199 to 206 labelled b_1(5)
- 198 to 199 labelled b_1(5)
- 198 to 226 labelled a_1(6)
- 201 to 202 labelled a_1(5)
- 202 to 203 labelled b_1(5)
- 200 to 201 labelled a_1(5)
- 204 to 191 labelled b_1(5)
- 203 to 204 labelled b_1(5)
- 206 to 207 labelled a_1(5)
- 207 to 208 labelled b_1(5)
- 207 to 210 labelled a_1(6)
- 205 to 206 labelled a_1(5)
- 209 to 172 labelled b_1(5)
- 209 to 195 labelled a_1(5)
- 209 to 192 labelled b_1(5)
- 208 to 209 labelled b_1(5)
- 211 to 212 labelled a_1(6)
- 212 to 213 labelled b_1(6)
- 210 to 211 labelled a_1(6)
- 214 to 196 labelled b_1(6)
- 213 to 214 labelled b_1(6)
- 227 to 228 labelled a_1(6)
- 228 to 229 labelled b_1(6)
- 226 to 227 labelled a_1(6)
- 230 to 210 labelled b_1(6)
- 229 to 230 labelled b_1(6)
- 229 to 234 labelled a_1(7)
- 235 to 236 labelled a_1(7)
- 236 to 237 labelled b_1(7)
- 234 to 235 labelled a_1(7)
- 238 to 212 labelled b_1(7)
- 237 to 238 labelled b_1(7)
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(x1)))) → A(a(x1))
A(c(x1)) → A(x1)
A(a(b(b(x1)))) → B(b(b(a(a(a(x1))))))
A(a(b(b(x1)))) → A(x1)
A(a(b(b(x1)))) → A(a(a(x1)))
B(c(x1)) → B(x1)
A(a(b(b(x1)))) → B(a(a(a(x1))))
A(a(b(b(x1)))) → B(b(a(a(a(x1)))))
The TRS R consists of the following rules:
a(a(b(b(x1)))) → b(b(b(a(a(a(x1))))))
a(c(x1)) → c(a(x1))
b(c(x1)) → c(b(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(x1)))) → A(a(x1))
A(c(x1)) → A(x1)
A(a(b(b(x1)))) → B(b(b(a(a(a(x1))))))
A(a(b(b(x1)))) → A(x1)
A(a(b(b(x1)))) → A(a(a(x1)))
B(c(x1)) → B(x1)
A(a(b(b(x1)))) → B(a(a(a(x1))))
A(a(b(b(x1)))) → B(b(a(a(a(x1)))))
The TRS R consists of the following rules:
a(a(b(b(x1)))) → b(b(b(a(a(a(x1))))))
a(c(x1)) → c(a(x1))
b(c(x1)) → c(b(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.